Circular Companion
Def?
論理$ \sf \Lambdaのシークエント計算体系$ \mathfrak{S}_\mathsf{\Lambda}を循環シークエント証明体系$ \mathfrak{S}^\mathrm{circ}_\mathsf{\Lambda}に拡張すると，別の論理$ \sf \Lambda'のシーケント証明体系$ \mathfrak{S}^\mathrm{circ}_\mathsf{\Lambda}と証明能力的に等価になることがある． すなわち$ \mathfrak{S}^\mathrm{circ}_\mathsf{\Lambda} \vdash \Gamma \iff \mathfrak{S}_\mathsf{\Lambda'} \vdash \Gammaが成り立つことがある．
Prop